Inference at * 1 0 2 
Iof proof for Lemma eq int cases test:

.....assertion..... NILNIL

1. A : Type
2. x : A
3. y : A
4. P : A
5. i : 
6. j : 
7. P(if (i = j) then x else y fi )
8.   Type
  (i = j)   

latex

 by ((Thin (-1)) 
CollapseTHEN (AddHiddenLabel `wf`)) 

latex

C1: .....wf..... NILNIL

C1: 7. P(if (i = j) then x else y fi )
C1:   (i = j)  
C.

Definitions

, t  T, (i = j), if b then t else f fi , f(a), , , x:AB(x), Type